active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
↳ QTRS
↳ DependencyPairsProof
active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
ACTIVE(c) → MARK(a)
MARK(f(X1, X2, X3)) → MARK(X3)
ACTIVE(f(a, b, X)) → F(X, X, X)
ACTIVE(f(a, b, X)) → MARK(f(X, X, X))
F(X1, mark(X2), X3) → F(X1, X2, X3)
F(X1, X2, mark(X3)) → F(X1, X2, X3)
MARK(f(X1, X2, X3)) → MARK(X1)
MARK(b) → ACTIVE(b)
F(active(X1), X2, X3) → F(X1, X2, X3)
MARK(a) → ACTIVE(a)
F(X1, active(X2), X3) → F(X1, X2, X3)
MARK(c) → ACTIVE(c)
MARK(f(X1, X2, X3)) → F(mark(X1), X2, mark(X3))
ACTIVE(c) → MARK(b)
F(X1, X2, active(X3)) → F(X1, X2, X3)
F(mark(X1), X2, X3) → F(X1, X2, X3)
MARK(f(X1, X2, X3)) → ACTIVE(f(mark(X1), X2, mark(X3)))
active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
ACTIVE(c) → MARK(a)
MARK(f(X1, X2, X3)) → MARK(X3)
ACTIVE(f(a, b, X)) → F(X, X, X)
ACTIVE(f(a, b, X)) → MARK(f(X, X, X))
F(X1, mark(X2), X3) → F(X1, X2, X3)
F(X1, X2, mark(X3)) → F(X1, X2, X3)
MARK(f(X1, X2, X3)) → MARK(X1)
MARK(b) → ACTIVE(b)
F(active(X1), X2, X3) → F(X1, X2, X3)
MARK(a) → ACTIVE(a)
F(X1, active(X2), X3) → F(X1, X2, X3)
MARK(c) → ACTIVE(c)
MARK(f(X1, X2, X3)) → F(mark(X1), X2, mark(X3))
ACTIVE(c) → MARK(b)
F(X1, X2, active(X3)) → F(X1, X2, X3)
F(mark(X1), X2, X3) → F(X1, X2, X3)
MARK(f(X1, X2, X3)) → ACTIVE(f(mark(X1), X2, mark(X3)))
active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
F(X1, active(X2), X3) → F(X1, X2, X3)
F(X1, X2, active(X3)) → F(X1, X2, X3)
F(mark(X1), X2, X3) → F(X1, X2, X3)
F(X1, mark(X2), X3) → F(X1, X2, X3)
F(X1, X2, mark(X3)) → F(X1, X2, X3)
F(active(X1), X2, X3) → F(X1, X2, X3)
active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(mark(X1), X2, X3) → F(X1, X2, X3)
F(active(X1), X2, X3) → F(X1, X2, X3)
Used ordering: Polynomial interpretation [25,35]:
F(X1, active(X2), X3) → F(X1, X2, X3)
F(X1, X2, active(X3)) → F(X1, X2, X3)
F(X1, mark(X2), X3) → F(X1, X2, X3)
F(X1, X2, mark(X3)) → F(X1, X2, X3)
The value of delta used in the strict ordering is 1/2.
POL(active(x1)) = 1/2 + (4)x_1
POL(mark(x1)) = 4 + (2)x_1
POL(F(x1, x2, x3)) = x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
F(X1, active(X2), X3) → F(X1, X2, X3)
F(X1, X2, active(X3)) → F(X1, X2, X3)
F(X1, mark(X2), X3) → F(X1, X2, X3)
F(X1, X2, mark(X3)) → F(X1, X2, X3)
active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(X1, X2, active(X3)) → F(X1, X2, X3)
F(X1, X2, mark(X3)) → F(X1, X2, X3)
Used ordering: Polynomial interpretation [25,35]:
F(X1, active(X2), X3) → F(X1, X2, X3)
F(X1, mark(X2), X3) → F(X1, X2, X3)
The value of delta used in the strict ordering is 1/8.
POL(active(x1)) = 1/2 + (4)x_1
POL(mark(x1)) = 1/4 + (2)x_1
POL(F(x1, x2, x3)) = (1/2)x_3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
F(X1, active(X2), X3) → F(X1, X2, X3)
F(X1, mark(X2), X3) → F(X1, X2, X3)
active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(X1, active(X2), X3) → F(X1, X2, X3)
Used ordering: Polynomial interpretation [25,35]:
F(X1, mark(X2), X3) → F(X1, X2, X3)
The value of delta used in the strict ordering is 8.
POL(active(x1)) = 4 + (2)x_1
POL(mark(x1)) = (2)x_1
POL(F(x1, x2, x3)) = (2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
F(X1, mark(X2), X3) → F(X1, X2, X3)
active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(X1, mark(X2), X3) → F(X1, X2, X3)
The value of delta used in the strict ordering is 8.
POL(mark(x1)) = 4 + (4)x_1
POL(F(x1, x2, x3)) = (2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
MARK(f(X1, X2, X3)) → MARK(X3)
ACTIVE(f(a, b, X)) → MARK(f(X, X, X))
MARK(f(X1, X2, X3)) → ACTIVE(f(mark(X1), X2, mark(X3)))
MARK(f(X1, X2, X3)) → MARK(X1)
active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
mark(f(X1, X2, X3)) → active(f(mark(X1), X2, mark(X3)))
mark(a) → active(a)
mark(b) → active(b)
mark(c) → active(c)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)